Many serious vulnerabilities in cyber systems arise from security flaws in software. To detect these flaws, organizations can invest enormous sums and significant human effort in testing and in certifying and accrediting the security of software. However, a serious limitation of testing, the most widely used method for obtaining evidence for certification and accreditation, is that by itself testing provides low confidence that the software is secure. Although code verification and analysis of abstract program models could significantly increase confidence in the security of software, this approach is currently viewed by those of ordinary skill in the art as too technically difficult, too expensive, and too time consuming. Therefore, obtaining high confidence that software code satisfies critical security properties remains a very difficult problem.
Recently, some commercial tools have been introduced that can be used, in addition to testing, to increase assurance in the security of software. Based on research in static analysis and similar techniques, these tools (e.g., PREfast, Coverity, Klocwork, CodeSonar, and Fortify) can detect code vulnerabilities automatically. Specifically, the class of security flaws which these tools uncover are application-independent, that is, errors and code vulnerabilities which do not depend on the application. Examples of the types of errors these tools can detect include null pointer deferences, format string problems, integer range errors, and buffer overflows. These tools have been effective in exposing and weeding out security errors in programs written in many languages, including C, Java, C++, and C#. An estimate is that the tools have exposed and led to the repair of tens of thousands of bugs, most of which traditional software testing would not have detected. One reason for the tools' success is their “pushbutton” nature, and another is user ease of understanding of the feedback they provide. To apply the tools, developers require neither significant skills nor special training.
Despite the success of these tools, both the research community and commercial tool vendors have paid far less attention to detecting a second important class of security flaws in software, application-specific errors. Application-specific errors are typically design errors that are violations of security properties specific to the application. Examples include violations of the allowed data flows and failure of a program to sanitize data areas after processing sensitive data in those areas. Some security experts estimate that, of the large number of security vulnerabilities that exist in current programs, approximately 50% belong to this second class of errors. However, detecting application-specific errors can be extremely difficult. Unlike the case of application-independent errors, where the developer can run a pushbutton tool to detect many code vulnerabilities automatically, the developer whose goal is to detect application-specific errors must define the specific security properties of interest. Specifying these properties can be a challenge, especially if the developer must express the properties in an unfamiliar language or logic.
Accordingly, a need remains in the art to develop an environment and a set of user-friendly, pushbutton tools that a developer can apply interactively to build a robust software program that satisfies developer-specified application-specific security properties.